app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
↳ QTRS
↳ Overlay + Local Confluence
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(filter2, app(f, x)), f)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(union, i), h)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(f, x)), f), x), xs)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(if_reach_2, app(app(eq, y), v)), x), y)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(if_reach_1, app(app(eq, x), u)), x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(reach, v), y)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(reach, x), y), i)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(reach, x), y), i)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i))
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(eq, y)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(reach, x), y)
APP(app(app(app(filter2, false), f), x), xs) → APP(filter, f)
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(app(union, i), h)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(filter2, app(f, x)), f), x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(or, app(app(app(app(reach, x), y), i), h))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(reach, x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), h)
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(eq, y), v)
APP(app(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(edge, u), v), h)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(union, i)
APP(app(eq, app(s, x)), app(s, y)) → APP(eq, x)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(if_reach_1, app(app(eq, x), u)), x), y)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(union, i)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(eq, x)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(if_reach_1, app(app(eq, x), u))
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(eq, x), u)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(reach, x), y)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(if_reach_2, app(app(eq, y), v))
APP(app(eq, app(s, x)), app(s, y)) → APP(app(eq, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(reach, v), y), app(app(union, i), h))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(reach, v)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
APP(app(app(app(filter2, true), f), x), xs) → APP(cons, x)
APP(app(filter, f), app(app(cons, x), xs)) → APP(filter2, app(f, x))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, v), y), app(app(union, i), h)), empty)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(if_reach_2, app(app(eq, y), v)), x)
APP(app(app(app(filter2, true), f), x), xs) → APP(filter, f)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(reach, x)
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(app(app(edge, x), y), app(app(union, i), h))
APP(app(app(app(filter2, true), f), x), xs) → APP(app(cons, x), app(app(filter, f), xs))
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(filter2, app(f, x)), f)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(union, i), h)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(f, x)), f), x), xs)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(if_reach_2, app(app(eq, y), v)), x), y)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(if_reach_1, app(app(eq, x), u)), x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(reach, v), y)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(reach, x), y), i)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(reach, x), y), i)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i))
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(eq, y)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(reach, x), y)
APP(app(app(app(filter2, false), f), x), xs) → APP(filter, f)
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(app(union, i), h)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(filter2, app(f, x)), f), x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(or, app(app(app(app(reach, x), y), i), h))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(reach, x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), h)
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(eq, y), v)
APP(app(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(edge, u), v), h)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(union, i)
APP(app(eq, app(s, x)), app(s, y)) → APP(eq, x)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(if_reach_1, app(app(eq, x), u)), x), y)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(union, i)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(eq, x)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(if_reach_1, app(app(eq, x), u))
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(eq, x), u)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(reach, x), y)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(if_reach_2, app(app(eq, y), v))
APP(app(eq, app(s, x)), app(s, y)) → APP(app(eq, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(reach, v), y), app(app(union, i), h))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(reach, v)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
APP(app(app(app(filter2, true), f), x), xs) → APP(cons, x)
APP(app(filter, f), app(app(cons, x), xs)) → APP(filter2, app(f, x))
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, v), y), app(app(union, i), h)), empty)
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(if_reach_2, app(app(eq, y), v)), x)
APP(app(app(app(filter2, true), f), x), xs) → APP(filter, f)
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(reach, x)
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(app(app(edge, x), y), app(app(union, i), h))
APP(app(app(app(filter2, true), f), x), xs) → APP(app(cons, x), app(app(filter, f), xs))
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(app(union, i), h)
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QDP
↳ QDP
APP(app(union, app(app(app(edge, x), y), i)), h) → APP(app(union, i), h)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
union1(edge(x, y, i), h) → union1(i, h)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
union(empty, x0)
union(edge(x0, x1, x2), x3)
reach(x0, x1, empty, x2)
reach(x0, x1, edge(x2, x3, x4), x5)
if_reach_1(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_1(false, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(false, x0, x1, edge(x2, x3, x4), x5)
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
union(empty, x0)
union(edge(x0, x1, x2), x3)
reach(x0, x1, empty, x2)
reach(x0, x1, edge(x2, x3, x4), x5)
if_reach_1(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_1(false, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(false, x0, x1, edge(x2, x3, x4), x5)
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
union1(edge(x, y, i), h) → union1(i, h)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
APP(app(eq, app(s, x)), app(s, y)) → APP(app(eq, x), y)
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QDP
APP(app(eq, app(s, x)), app(s, y)) → APP(app(eq, x), y)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
eq1(s(x), s(y)) → eq1(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
union(empty, x0)
union(edge(x0, x1, x2), x3)
reach(x0, x1, empty, x2)
reach(x0, x1, edge(x2, x3, x4), x5)
if_reach_1(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_1(false, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(false, x0, x1, edge(x2, x3, x4), x5)
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
union(empty, x0)
union(edge(x0, x1, x2), x3)
reach(x0, x1, empty, x2)
reach(x0, x1, edge(x2, x3, x4), x5)
if_reach_1(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_1(false, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(false, x0, x1, edge(x2, x3, x4), x5)
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
eq1(s(x), s(y)) → eq1(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, v), y), app(app(union, i), h)), empty)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), h)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
APP(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
APP(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, v), y), app(app(union, i), h)), empty)
APP(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(reach, x), y), i), h)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → APP(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(x, y, i, h)
if_reach_11(true, x, y, edge(u, v, i), h) → if_reach_21(eq(y, v), x, y, edge(u, v, i), h)
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(v, y, union(i, h), empty)
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
union(empty, x0)
union(edge(x0, x1, x2), x3)
reach(x0, x1, empty, x2)
reach(x0, x1, edge(x2, x3, x4), x5)
if_reach_1(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_1(false, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(false, x0, x1, edge(x2, x3, x4), x5)
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
or(true, x0)
or(false, x0)
reach(x0, x1, empty, x2)
reach(x0, x1, edge(x2, x3, x4), x5)
if_reach_1(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_1(false, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(true, x0, x1, edge(x2, x3, x4), x5)
if_reach_2(false, x0, x1, edge(x2, x3, x4), x5)
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(x, y, i, h)
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
if_reach_11(true, x, y, edge(u, v, i), h) → if_reach_21(eq(y, v), x, y, edge(u, v, i), h)
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(v, y, union(i, h), empty)
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
union(empty, x0)
union(edge(x0, x1, x2), x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(x, y, i, h)
Used ordering: Polynomial interpretation with max and min functions [25]:
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
if_reach_11(true, x, y, edge(u, v, i), h) → if_reach_21(eq(y, v), x, y, edge(u, v, i), h)
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(v, y, union(i, h), empty)
POL(0) = 0
POL(edge(x1, x2, x3)) = 1 + x3
POL(empty) = 0
POL(eq(x1, x2)) = 0
POL(false) = 0
POL(if_reach_11(x1, x2, x3, x4, x5)) = x4 + x5
POL(if_reach_21(x1, x2, x3, x4, x5)) = x4 + x5
POL(reach1(x1, x2, x3, x4)) = x3 + x4
POL(s(x1)) = 0
POL(true) = 0
POL(union(x1, x2)) = 1 + x1 + x2
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
if_reach_11(true, x, y, edge(u, v, i), h) → if_reach_21(eq(y, v), x, y, edge(u, v, i), h)
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(v, y, union(i, h), empty)
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
union(empty, x0)
union(edge(x0, x1, x2), x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
if_reach_21(false, x, y, edge(u, v, i), h) → reach1(v, y, union(i, h), empty)
Used ordering: Polynomial interpretation with max and min functions [25]:
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
if_reach_11(true, x, y, edge(u, v, i), h) → if_reach_21(eq(y, v), x, y, edge(u, v, i), h)
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
POL(0) = 0
POL(edge(x1, x2, x3)) = 1 + x3
POL(empty) = 0
POL(eq(x1, x2)) = 0
POL(false) = 0
POL(if_reach_11(x1, x2, x3, x4, x5)) = x4 + x5
POL(if_reach_21(x1, x2, x3, x4, x5)) = x4 + x5
POL(reach1(x1, x2, x3, x4)) = x3 + x4
POL(s(x1)) = 0
POL(true) = 0
POL(union(x1, x2)) = x1 + x2
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
if_reach_11(true, x, y, edge(u, v, i), h) → if_reach_21(eq(y, v), x, y, edge(u, v, i), h)
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
union(empty, x0)
union(edge(x0, x1, x2), x3)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
union(empty, x0)
union(edge(x0, x1, x2), x3)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
union(empty, x0)
union(edge(x0, x1, x2), x3)
union(empty, x0)
union(edge(x0, x1, x2), x3)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
if_reach_11(false, x, y, edge(u, v, i), h) → reach1(x, y, i, edge(u, v, h))
reach1(x, y, edge(u, v, i), h) → if_reach_11(eq(x, u), x, y, edge(u, v, i), h)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
APP(app(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(f, x)), f), x), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(app(eq, 0), 0) → true
app(app(eq, 0), app(s, x)) → false
app(app(eq, app(s, x)), 0) → false
app(app(eq, app(s, x)), app(s, y)) → app(app(eq, x), y)
app(app(or, true), y) → true
app(app(or, false), y) → y
app(app(union, empty), h) → h
app(app(union, app(app(app(edge, x), y), i)), h) → app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) → false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, true), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(app(if_reach_2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(if_reach_1, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(if_reach_2, true), x), y), app(app(app(edge, u), v), i)), h) → true
app(app(app(app(app(if_reach_2, false), x), y), app(app(app(edge, u), v), i)), h) → app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(eq, 0), 0)
app(app(eq, 0), app(s, x0))
app(app(eq, app(s, x0)), 0)
app(app(eq, app(s, x0)), app(s, x1))
app(app(or, true), x0)
app(app(or, false), x0)
app(app(union, empty), x0)
app(app(union, app(app(app(edge, x0), x1), x2)), x3)
app(app(app(app(reach, x0), x1), empty), x2)
app(app(app(app(reach, x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_1, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, true), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(app(app(app(if_reach_2, false), x0), x1), app(app(app(edge, x2), x3), x4)), x5)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
From the DPs we obtained the following set of size-change graphs: